es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Try(e1)  (j  L)  ((j = loc(e1)))  (loc(the rcv(wanted message from e1 to j)) = j)) 

latex

Definitions	, t.2, t.1, t  T, IdLnk, destination(l), "$x", the rcv(wanted message from e1 to j), P  Q, Id, x:A. B(x), xL. P(x), P & Q, A c B, Try(e), fischer(L)
Lemmas	event system wf, fischer wf, es-E wf, f-try wf, l member wf, es-loc wf, Id wf, not wf, es-loc-first-from